00100	
00200	
00300	(DEFPROP TRSUBST1 
00400	 (LAMBDA(X Y Z)
00500	  (COND ((ATOM Z) Z)
00600		((ATOM (CAR Z)) (CONS (CAR Z) (TRSUBST1 X Y (CDR Z))))
00700		((EQ (CAAR Z) (QUOTE ←))
00800		 (COND ((EQUAL Y (CADDAR Z))
00900			(CONS (LIST (QUOTE ←) X Y) (CONS (LIST (QUOTE ←) (CADAR Z) X) (TRSUBST1 X Y (CDR Z)))))
01000		       (T (CONS (CAR Z) (TRSUBST1 X Y (CDR Z))))))
01100		(T (CONS (TRSUBST1 X Y (CAR Z)) (TRSUBST1 X Y (CDR Z)))))) 
01200	EXPR)
01300	
01400	(DEFPROP VSUB1 
01500	 (LAMBDA(RL PL)
01600	  (PROG (CRL SPL DONE CRL1)
01700		(COND ((NULL PL) (RETURN NIL)))
01800		(SETQ CRL RL)
01900		(SETQ SPL PL)
02000	   VS1  (COND (DONE (GO VS3)))
02100		(SETQ DONE T)
02200		(SETQ CRL (RECSUB1 CRL CRL))
02300		(GO VS1)
02400	   VS3  (COND ((NOT DONE) (RETURN SPL)))
02500		(SETQ CRL1 CRL)
02600		(SETQ DONE NIL)
02700	   VS5  (COND ((NULL CRL1) (GO VS3)))
02800	(SETQ DONE NIL)
02900		(SETQ SPL (TRSUBST1 (CDAR CRL1) (CAAR CRL1) SPL))
03000		(SETQ CRL1 (CDR CRL1))
03100		(GO VS5))) 
03200	EXPR)
03300	
03400	(DEFPROP WHILASSEM 
03500	 (LAMBDA(BP IP CL CT)
03600	  (PROG (ALP ALS PA Y Z W R SASG SASGR TE ALF BET WFT ALFT RP)
03700		(PRINT (QUOTE L37410))
03800		(PRINT BP)
03900		(PRINT IP)
04000		(PRINT CL)
04100		(PRINT CT)
04200		(PRINT (QUOTE L37415))
04300		(PRINT (THV SASSERTLITS))
04400		(PRINT (THV ASSERTLITS))
04500		(SETQ WFT (THV FT))
04600		(PRINT (QUOTE L37425))
04700		(PRINT CL)
04800		(PRINT WFT)
04900		(SETQ IP (REVERSE IP))
05000	   WH2  (SETQ PA (CAR CL))
05100		(PRINT (QUOTE L37432))
05200		(PRINT PA)
05300		(PRINT WFT)
05400		(SETQ Y (READLIST (APPEND (LIST (QUOTE Y)) (EXPLODE (THSETQ (THV YN) (ADD1 (THV YN)))))))
05500		(SETQ Z (READLIST (APPEND (LIST (QUOTE Z)) (EXPLODE (THSETQ (THV ZN) (ADD1 (THV ZN)))))))
05600		(COND ((CDDR PA) (SETQ ALF (CAR PA)) (SETQ BET (CADR PA)))
05700		      (T (SETQ ALF (CAAR PA)) (SETQ BET (CADAR PA))))
05800		(SETQ ALFT (COND ((CDDAR WFT) (CAAR WFT)) (T (CAAAR WFT))))
05900		(SETQ BP (CONS (LIST (QUOTE ←) Y ALFT) BP))
06000		(SETQ LIFOL
06100		      (CONS (COND ((THASVAL (THV NT)) (SUBST Y ALFT (SUBST Z ALF (CAR LIFOL))))
06200				  (T (SUBST Y ALFT (SUBST Z BET (CAR LIFOL)))))
06300			    (CDR LIFOL)))
06400		(SETQ IP (APPEND IP (LIST (LIST (QUOTE ←) Y Z))))
06500		(SETQ ALP (CONS (CONS ALF Y) ALP))
06600		(SETQ ALS (CONS (CONS BET Z) ALS))
06700		(PRINT (QUOTE L37456))
06800		(PRINT PA)
06900		(COND ((CDDR PA) (SETQ SASG (APPEND (LIST (LIST (QUOTE ←) Z (CADDR PA))) SASG)) (GO WH4)))
07000		(SETQ R (CADR PA))
07100		(SETQ R
07200		      (APPEND (LIST (CAR R))
07300			      (COND ((CDR R) (COND ((CDDR R) (LIST (CADR R) (CADDR R))) (T (LIST (CADR R)))))
07400				    (T NIL))))
07500		(SETQ W (READLIST (APPEND (LIST (QUOTE W)) (EXPLODE (THV ZN)))))
07600		(SETQ RP R)
07700		(SETQ R (SUBST W BET R))
07800		(COND ((EQUAL R RP) (SETQ R (SUBST W ALF R))))
07900		(SETQ SASGR (APPEND (LIST (LIST (QUOTE IF) R (QUOTE THEN) (LIST (QUOTE ←) Z W))) SASGR))
08000	   WH4  (SETQ CL (CDR CL))
08100		(SETQ WFT (CDR WFT))
08200		(COND (CL (GO WH2)))
08300		(PRINT (QUOTE L38525))
08400		(PRINT ALP)
08500		(PRINT ALS)
08600		(PRINT SASG)
08700		(PRINT SASGR)
08800		(SETQ ALP (DEQ ALP))
08900		(SETQ ALS (DEQ ALS))
09000		(SETQ SASG (REVERSE (VSUB ALP SASG)))
09100		(SETQ SASGR (REVERSE (VSUB ALP SASGR)))
09200		(SETQ IP (VSUB1 ALS IP))
09300		(SETQ IP (VSUB ALP IP))
09400		(SETQ CT (VSUB ALP CT))
09500		(SETQ TE
09600		      (SUBPLANL (APPEND (LIST (LIST (QUOTE WHILE) (CONS NEGSGN CT) (QUOTE DO) (APPEND  IP SASGR)))
09700					(APPEND SASGR BP))
09800				(THV PLANL)))
09900		(PRINT TE)
10000		(RETURN TE))) 
10100	EXPR)
10200	
10300	(DEFPROP ALS 
10400	 (NIL ((H* (G* NIL*) NIL*) . Z1)) 
10500	VALUE)
10600	
10700	(DEFPROP IP 
10800	 (NIL (IF (VAR (G* NIL*))
10900	 	  THEN
11000		  (PROC2 Z NIL* (G* NIL*))
11100	 	  ELSE
11200		  ((← Z (H* (G* NIL*) NIL*)) (VARNOT Z NIL* (G* NIL*))))
11300	      (← Y1 Z1)) 
11400	VALUE)